1. Technical Field
The present disclosure generally relates to verification techniques for logic design and in particular to techniques for performing diameter bounding for complex feed-forward components in a logic design.
2. Description of the Related Art
Design verification refers to the process of establishing the correctness of a given logic design. Due to the complexity of modern logic designs, formal verification methods are gaining widespread use to augment the coverage shortcomings of simulation-based validation approaches. Formal verification methods are exhaustive, and thus are guaranteed to expose all possible logic flaws. In contrast, simulation-based validation is incomplete, and thus may fail to expose certain logic flaws (or bugs). While formal verification is a very powerful technology, formal verification generally requires exponential resources with respect to design size and thus is often only applicable to smaller design components. Semi-formal methods attempt to leverage the exhaustive bug-hunting power of formal verification techniques in an incomplete way. For example, symbolic simulation techniques exhaustively analyze design behavior for a specific number of bounded time-frames. Algorithms to perform such bounded formal verification are often of much greater scalability than those for unbounded formal verification. However, the bounded nature of this approach implies incompleteness. That is, performing a check for time-frames 0 to k does not necessarily imply that no violation will occur at time-frames greater than k.
With some of these bounded verification techniques, a diameter can be established. The term “diameter” refers to the number of time-frames necessary to exhaustively analyze all design behaviors. If the diameter of a design is known, the diameter can enable the use of more scalable bounded verification algorithms in a complete way. Unfortunately, techniques to tightly estimate design diameter are generally as complex as the process of verification itself.